topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
A uniform locale is to a uniform space as a locale is to a topological space.
While an ordinary uniform space is defined directly in terms of subsets, and the underlying topology then constructed secondarily, in the absence of an underlying set it seems more convenient to define a uniform locale as additional structure on a given locale, together with an additional axiom which essentially says “the underlying topology is the same as the one we started with.”
For any and any sublocale of , with inclusion map , we write for the image of of under the projection . If is overt (such as if is an open part of and is overt, or if excluded middle holds), then is an open part of , and can equivalently be defined as , where means “ is positive”. Otherwise, it is merely a sublocale.
Similarly, if , we write for the image of under the projection . If is overt, this is an open part of ; otherwise it is merely a sublocale. We also write for the pullback of along the twist map .
An [open] cover of a locale is a collection of open parts of whose join is . For covers , we define:
refines , written , if every element of is in some element of .
; this is also a cover.
, and .
For , we write (see above definition). If is overt (such as if is overt, such as if excluded middle holds), this is equivalent to , where positive is in the sense of positive element.
.
We now define a covering uniformity on a locale to be a collection of covers, called uniform covers, such that
If is a uniform cover and , then is a uniform cover.
The cover is a uniform cover and if are uniform covers, then so is .
If is a uniform cover, there exists a uniform cover such that .
The collection of uniform covers is admissible: for any open part , we have
The last condition is the one saying that “the induced topology is again the topology of .”; the other conditions correspond precisely to the uniform-cover definition of a uniform topological space.
An entourage (Picado and Pultr, Section XII.1.1) is an open part such that is an open cover of .
An entourage uniformity (Picado and Pultr, Section XII.2.3) on a locale is a collection of entourages such that:
If is an entourage and , then is also an entourage.
The open part is an entourage and if and are entourages, then so is .
If is an entourage, then so is .
For any entourage , there exists an entourage such that . The sublocale is not always open, but we can still ask it to be contained in the open sublocale .
The collection of uniform entourages is admissible: for any we have .
Given an entourage on a locale , we define an open cover by setting
Given an entourage uniformity , we construct a covering uniformity out of it by taking all open covers that are refined by some .
Given an open cover , we construct an entourage by setting $$
Given a covering uniformity , we construct an entourage uniformity out of it by taking all entourages that contain some .
Theorem XII.3.3.4 in Picado and Pultr shows that the above correspondence is bijective. Furthermore, the categories of entourage uniform locales and covering uniform locales are equivalent (Corollary XII.3.4.3 in the cited book). However, since their book uses classical logic throughout, it is not entirely clear whether the same equivalence holds constructively.
A locale admits a uniformity if and only if it is completely regular (Picado-Pultr, Theorem 2.8.2).
Uniformities are closed under unions, so any completely regular locale admits a largest uniformity, the fine uniformity.
The fine uniformity consists of all normal covers? (alias numerable covers), where a cover is normal if there is a sequence of covers such that and refines .
On a compact regular locale the system of all covers forms a uniformity. Maps out of compact regular locales are automatically uniform.
A uniform locale is complete if every dense uniform embedding is an isomorphism of uniform locales.
The category of complete uniform locales is a reflective subcategory of uniform locales. The reflection functor is known as the completion functor.
Concretely, the completion of a uniform locale with a system of uniform covers can be described as follows. Its opens are downward-closed subsets of the underlying frame of that satisfy the following saturation conditions:
If for some we have , then also . Here means that there is such that .
If for some and we have , then also .
Every compact regular locale is complete. The fine uniformity on a paracompact locale is complete.
Isbell’s theorem states that a locale is paracompact if and only if it admits a complete uniformity.
A completely regular locale is compact if and only if it admits a complete uniformity that has a basis in which all covers are finite.
A detailed treatment of uniform locales can be fund in
The following paper developes covering uniformities constructively, and includes citations to several other papers that do it classically:
These ideas are developed further in
A constructive and predicative theory in the programme of formal topology can be found here:
Giovanni Curi, On the collection of points of a formal space, Annals of Pure and Applied Logic* 137 1-3 (2006) 126-146 doi:10.1016/j.apal.2005.05.019
Giovanni Curi; Constructive metrisability in point-free topology; Theoretical Computer Science 305 (2003) 1–3, 85–109.
Last revised on March 29, 2024 at 23:30:21. See the history of this page for a list of all contributions to it.